% $Revision$
% $Id$


\chapter{Expressions} \label{expressions} \index{expression}

In this chapter, we describe the syntax and informal semantics of \frege{} \emph{expressions} and give translations into more basic expressions, where appropriate.
Free variables and constructors used in these translations refer to entities defined by the standard package \texttt{frege.Prelude}.

%The various syntactical expression categories form a syntactical hierarchy, such that 
%all \hyperref[termexp]{terms} are \hyperref[primexp]{primary expressions}, 
%all primary expressions are \hyperref[unaryexp]{unary expressions},
%all unary expressions are \hyperref[funapp]{function applications},
%all function applications are \hyperref[topex]{operand expressions},
%all operand expressions are \hyperref[binex]{infix expressions}
%and all infix expressions are general \hyperref[annex]{expressions}.

\section{Terms} \index{expression!term} \label{termexp}

\begin{flushleft}
\rul{term} \nont{qvarid} \gcom{variable}
  \alt{} \nont{qconid}  \gcom{constructor}
  \alt{} \nont{qconid}  \sym{\{} \nont{initfields} \sym{\}} \gcom{record construction}
  \alt{} \nont{literal}
  \alt{} \regex{\_} \gcom{a single underscore}
  \alt{} \sym{(} \nont{qlexop} \sym{)}
  \alt{} \sym{(} \nont{qunop} \sym{)}
  \alt{} \nont{section}
  \alt{} \sym{(} \sym{)} \gcom{unit constructor}
  \alt{} \nont{tuple} \gcom{see \autoref{tupleterm}}
  \alt{} \nont{list}  \gcom{see \autoref{listterm}}\\
\rul{initfields} \liste{\nont{initfield}}{,}\\
\rul{initfield} \nont{varid} \opt{\sym{=} \nont{expr}}\\
\end{flushleft}

The most basic expressions are variables, value constructors and literals.
Variables stand for the values they are bound to, often these values are functions.
Likewise, a value constructor may stand for a value or for a function that constructs values depending on other values.

Constructors that were defined with field labels can be applied to a list of field initializations enclosed in braces. 
Exactly the field labels that belong to the constructor must be specified. 
If the expression is omitted, the value of the variable currently in scope that has the same name as the field is used (punning). 
The expression is translated to an ordinary constructor application by reordering the expressions given for the fields so that they appear in the same order as in the constructor definition.

\trans{

\begin{tabular}{lcl}
Con \{ $\cdots$, $a$, $\cdots$ \} & $=$ & Con \{ $\cdots$, $a=a$, $\cdots$ \}\\
Con \{ $a =x_a$, $c =x_c$, $b = x_b$ \} & $=$ & (Con $x_c$ $x_b$ $x_a$)\\
& & if the order of the fields in the\\
& & constructor was $c$, $b$, $a$ \\
\end{tabular}

}

\hasdiff{Values for all fields must be given, it is not allowed to leave out fields.}

Literals stand for the value they represent.

A single underscore is technically a variable, yet can only appear in pattern bindings, where it signals that the corresponding part of a value is not bound, and in primary expressions.

Sometimes one needs to refer to a function whose name is an operator lexically. Any unary or infix operator may be used as a variable or constructor by enclosing it in parentheses.
Another way to put this is to say that an operator enclosed in parentheses looses its syntactic properties.

\trans{

\begin{tabular}{lcl}
($op$) & $=$ & \emph{the function defined by $op$}, where $op$ is an operator\\
$e_1$ $op$ $e_2$ & $=$ & ($op$) $e_1$ $e_2$, where $op$ is a binary operator\\
$f$ $op$ $e$ & $=$ & $f$ (($op$) $e$), where $op$ is an unary operator\\
\end{tabular}
}

An expression of arbitrary complexity becomes a term syntactically when enclosed in parentheses.

Certain constructs exist to deal with partially applied binary operators and the data types "built in" the language, namely tuples and lists. They all are terms syntactically and are explained in the following subsections.

\subsection{Sections} \index{expression!term!section}

\begin{flushleft}
\rul{section} \sym{(} \nont{binex} \nont{lexop} \sym{)}
 \alt{} \sym{(} \nont{lexop} \nont{expr} \sym{)}
\end{flushleft}

So called \emph{sections} are means of creating functions on the fly by providing the first or second argument to an infix operator (see \autoref{operator}), that is, to a function that takes (at least) two arguments.

For example, the expression $(e < 42)$ denotes one of the values \term{true} or \term{false}, depending on the value of \emph{e}.
We can now abstract out either side of the expression to get two functions:
\begin{enumerate}
\item a function that checks whether its argument is lower than 42
\item a function that checks whether \emph{e} is lower than its argument
\end{enumerate}
Sections permit us to do that syntactically by just leaving out the subexpression we abstract from. We write $( < 42)$ for the first function and $(e <)$ for the second.

\trans{
The following identities hold:
\begin{center}
\begin{tabular}{lcl}
(- e)& $=$ & negate e\\
(`op` e) & $=$ & $\backslash$x \arrow{} x `op` (e)\\
(e -) & $=$ & $\backslash$x \arrow{} e - x\\ 
(e `op`) & $=$ & $\backslash$x \arrow{} e `op` x $=$ (`op`) (e)
\end{tabular}
\end{center}
where \emph{`op`} is a binary operator, \emph{e} is an expression and \emph{x} is a variable that does not occur in \emph{e}
}

The precedence of the operator in a section where the operator comes first is irrelevant. It is so as if the subexpression in the section were always written in parentheses.

However, if the operator stands on the right, its precedence must be taken into account.

For example,the function $(*1+x)$ multiplies its argument with $(1+x)$. But $(1+x*)$ is a syntax error. It must be written like this: $((1+x)*)$.

\subsubsection{Special role of the subtraction/negation operator}

The operator \term{$-$} is treated specially in the grammar. It can act as binary operator, indicating subtraction, or as an unary operator, in which case it indicates negation. 
The token \term{$-$} will \emph{always} refer to the Prelude definition of either subtraction or negation, it is not possible to redefine or qualify it.

Because
$e1-e2$ parses as an infix application of the binary operator \term{$-$}, one must write $e1 (-e2)$ for the alternative
parsing. Similarly, $(-)$ is syntax for $(\backslash x \backslash y$ \arrow{} $x-y)$, 
as with any infix operator, and does not denote
$(\backslash x$ \arrow{} $-x)$ -- one must use \term{negate} for that.

Finally, $(- e)$ is not a section, but an application of prefix negation,
as described above. However, there is a \term{subtract} function defined in the Prelude such
that $(subtract$  $e)$ is equivalent to the disallowed section. The expression $(+ (- e))$ can serve the
same purpose.


\subsection{Unit}

The \emph{unit expression} \sym{()} has type () (see \autoref{unittype}); it is the only value of that type.

\subsection{Tuples} \label{tupleterm} \index{expression!term!tuple}

For a discussion of tuple types see \autoref{tupletypes}.

\begin{flushleft}
\rul{tuple} \nont{tupleconstructor} \oder{} \nont{n-tuple}\\
\rul{tupleconstructor} \sym{(,}\some{\sym{,}}\sym{)}\\
\rul{n-tuple} \sym{(}\nont{expr}\sym{,} \liste{\nont{expr}}{\sym{,}}\sym{)}\\
\end{flushleft}

Tuples are written $(e_1, ..., e_k)$ where $2\le k \le 26$.
The constructor for an $n$-tuple is denoted by $(,...,)$ where there are $n-1$ commas.
\trans{The following identities hold:\\
\begin{tabular}{lcl}
($e_1$, $e_2$) & $=$ & (,) $e_1$ $e_2$\\
($e_1$, $e_2$, $e_3$)& $=$ & (,,) $e_1$ $e_2$ $e_3$\\
$...$ and so forth up to & & \\
($e_1$, $e_2$, ..., $e_{26}$) & $=$ & (,,,,,,,,,,,,,,,,,,,,,,,,,,) $e_1$ $e_2$ ... $e_{26}$\\
\end{tabular}
}

Tuple construction does not cause evaluation of the tuple elements $e_i$. We say that tuple construction is lazy.

\subsection{Lists} \label{listterm} \index{expression!term!list}

Lists are also discussed in \autoref{listtype}.

\begin{flushleft}
\rul{list} \sym{[]}  \gcom{constructor for the empty list}
  \alt{} \bracka{}\liste{\nont{expr}}{\sym{,}}\brackz{}
  \alt{} \bracka{}\nont{expr}\opt{\sym{,} \nont{expr}} \sym{..} \opt{\nont{expr}}\brackz{} \gcom{arithmetic sequence} 
  \alt{} \bracka{}\nont{expr} \sym{$|$} \liste{\nont{dlcqual}}{\sym{,}}\brackz{} \gcom{list comprehension}\\
\rul{dlcqual} \nont{pattern} \term{$\leftarrow$} \nont{expr}
  \alt \nont{expr}
  \alt  \texttt{let} \bracea{} \liste{\nont{decl}}{;} \bracez{}
\end{flushleft}

Lists are written $[e_1, \cdots, e_k]$, where $k>=1$. The list constructor \sym{:} as well as the constructor for the empty list \sym{[]} is considered part of the language syntax and cannot be hidden or redefined.

\trans{The following identity holds:\\
$[e_1, e_2, \cdots, e_k] = e_1 : (e_2 :( \cdots ( e_k : [] )))$\\
The types of $e_1$ trough $e_k$ must all be the same (call it $t$), and the type of the expression is $[t]$.
}

\subsubsection{Arithmetic Sequences} \index{expression!term!arithmetic sequences} \index{list!arithmetic sequences}
\label{aseq}

The \emph{arithmetic sequence} \bracka{}$e_1$ \opt{, $e_2$} .. \opt{$e_3$}\brackz{} 
denotes a list of values of type $t$, 
where each of the $e_i$ has type $t$, and $t$ is an \hyperref[instance]{instance} of type class \term{Enum}.

\trans{Arithmetic sequences satisfy these identities:\\
\begin{tabular}{lcl}
\bracka{}$e_1$ \sym{..}\brackz{} & = & enumFrom $e_1$\\
\bracka{}$e_1$, $e_2$ \sym{..}\brackz{} & = & enumFromThen $e_1$ $e_2$\\
\bracka{}$e_1$ \sym{..} $e_3$\brackz{} & = & enumFromTo $e_1$ $e_3$\\
\bracka{}$e_1$, $e_2$ \sym{..} $e_3$\brackz{} & = & enumFromThenTo $e_1$ $e_2$ $e_3$\\
\end{tabular}
}

The semantics of arithmetic sequences therefore depends entirely on the \hyperref[instdcl]{instance declaration}
for the type $t$ .

The intended semantics for \emph{enumFrom} is to evaluate to a list that consists of the start element $e_1$, followed by all its successors in ascending order, while \emph{enumFromTo} restricts the sequence of successors up to and including $e_3$. The \emph{enumFromThen} and \emph{enumFromThenTo} functions are variants thereof that produce successive elements whose ordinal values differ by the same amount as the ordinal values of the first two. Hence

\exq{/enumFrom a = enumFromThen a (succ a)/}

It is also possible to create decreasing sequences, by giving an $e_2$ that is smaller than $e_1$.

\hasdiff{
In \frege{}, the types \texttt{Double} and \texttt{Float} have no standard instances for type class \texttt{Enum}, hence floating point arithmetic sequences are not available out of the box.

Sequences for floating point numbers are best created using the \emph{iterate} function.
}

\subsubsection{List Comprehensions} \index{expression!term!list comprehension} \index{list!comprehension}

List comprehension is a powerful notation to describe lists based on other lists. It has the form $[ e | q_1, \cdots, q_n]$, where $n>=1$ and the qualifiers $q_i$ are either
\begin{itemize}
\item \emph{generators} of the form $p \leftarrow{} e$, where $p$ is a pattern (see \autoref{patterns}) of type $t$ and $e$ is an expression of type $[t]$.
\item \emph{guards}, which are arbitrary expressions of type \texttt{Bool}.
\item \emph{local bindings} \texttt{let} \bracea{} \liste{\nont{decl}}{;} \bracez{}\\
Because list comprehension qualifiers are separated with commas and the keyword \texttt{in} is missing, 
it is not possible to invoke the layout rule by omitting the braces in this case. 
For convenience, a single binding \texttt{let} \bracea{} \nont{decl} \bracez{}
can be written simply \nont{decl}.
\end{itemize}

Such a list comprehension returns the list of elements produced by evaluating $e$ in the successive environments created by the nested, depth-first evaluation of the generators in the qualifier list.
Binding of variables occurs according to the normal pattern matching rules (see \autoref{patternmatch}), and if a match fails then that element of the list is simply skipped over.
Thus:

\mint[bgcolor=gruen]{fr}{[ x | (2, x) <- [(1, 'a'), (2, 'b'), (3, 'c'), (2, 'd')] ]}

yields the list \texttt{['b', 'd']}.

If a qualifier is a guard, it must evaluate to \sym{true} for the previous pattern match to succeed.
As usual, bindings in list comprehensions can shadow those in outer scopes; for example, there is no difference between functions \term{f} and \term{g} below:

\begin{minted}[bgcolor=gruen]{fr}

f x = [ x | x <- x, x <- x ]
g x = [ z | y <- x, z <- y ]  -- same as before

\end{minted}


\trans{
A list comprehension can be rewritten by the following translation scheme:\\
\begin{tabular}{lcl}
LC [e $|$ Q ] & = & TQ [e $|$ Q ] []\\
TQ [e $|$ ] L & = & \texttt{(e) : L}\\
TQ [e $|$ b, Q] L & = & \texttt{if b then} TQ [e $|$ Q]  L \texttt{else L}\\
TQ [ e $|$ p $\leftarrow$ xs, Q ] L & = &\texttt{let}\\
& &\hspace{1cm}\texttt{h [] = L}\\
& &\hspace{1cm}\texttt{h (p:ys) = }TQ [e $|$ Q] (h ys)\\
& &\hspace{1cm}\texttt{h (\_:ys) = h ys}\\
& &\texttt{in h xs}\\
TQ [ e $|$ \texttt{let \bracea{}} \nont{decls} \texttt{\bracez{}}, Q ] L & = &  
\texttt{let \bracea{}} \nont{decls} \texttt{\bracez{} in} TQ [e $|$ Q] L\\
\end{tabular}\\
where $e$ ranges over expressions, $p$ ranges over patterns, $xs$ ranges over list valued expressions, $b$ ranges over boolean expressions, $Q$ ranges over sequences of qualifiers and \texttt{h} and \texttt{ys} are fresh variables.
}

\paragraph{Example}
Let's translate the following program fragment:

\begin{minted}[bgcolor=gruen]{fr}
nums = [1,2,3,4,5,6,7,8,9,10]
squares = [ n*n | n <- nums, n > 4 ]
\end{minted}

We have first \ex{nums = 1:2:3:4:5:6:7:8:9:10:[]}
Note that we omitted the parentheses from the translation rule, which is ok since \sym{:} is right associative.

Next we apply translation scheme LC to the list comprehension. This gives us\\
TQ \ex/[ n*n | n <- nums, n > 4 ] []/

The TQ scheme has 4 rules that cover all possible forms of a qualifier list. Our qualifier list starts with a generator, thus we have to apply the 3rd rule substituting \texttt{n*n} for $e$, \texttt{n} for $p$ and \texttt{nums} for $xs$. $L$ is the empty list and $Q$ stands for the rest of our qualifier list, which is \texttt{n>4}.
We get

\begin{code}
squares = let
   h1 [] = []
   h1 (n:ys1) = ... // translation of TQ [ n*n | n>4 ] (h1 ys1)
   h1 (_:ys1) = h1 ys1
 in h1 nums
\end{code}

We now have to translate TQ \ex/[ n*n | n > 4 ] (h1 ys1)/ by the second rule, since the qualifier list starts with a guard. We substitute $e$ with \texttt{n*n} as before, $b$ is the guarding expression \texttt{n>4}, $Q$ is empty and $L$ stands for the expression \texttt{(h1 ys1)}.
The result is 
\ex{if n>4 then} \emph{TQ} \ex{ [ n*n | ] (h1 ys1) else (h1 ys1)}

and after translating the last remaining TQ scheme by the first rule, the complete program is

\begin{code}
nums = 1:2:3:4:5:6:7:8:9:10:[]
squares = let
   h1 [] = []
   h1 (n:ys1) = if n>4 then (n*n) : (h1 ys1) else (h1 ys1)
   h1 (_:ys1) = h1 ys1
 in h1 nums
\end{code}



\section{Primary Expression} \label{primexp} \index{expression!primary}

\emph{Primary expressions} are used for invocation of member functions, field selection, field update, array access and array update using a concise notation that will be translated by the compiler. The translations are given below in the usual way.

\begin{flushleft}
\rul{primary} \nont{term}
  \alt \nont{primary}\sym{.} \nont{varid} \gcom{member function application}
  \alt \nont{primary}\sym{.} \nont{lexop} \gcom{member function application}
  \alt \nont{primary}\sym{.} \nont{unop}  \gcom{member function application}
  \alt \nont{qualifier} \sym{\{}\nont{varid} \sym{?}\sym{\}} \gcom{general field existence function}
  \alt \nont{qualifier} \sym{\{}\nont{varid} \sym{=}\sym{\}} \gcom{general field update function}
  \alt \nont{qualifier} \sym{\{}\nont{varid} \sym{<-}\sym{\}} \gcom{general field change function}
  \alt \nont{qualifier} \sym{\{}\liste{\nont{field}}{\sym{,}}\sym{\}} \gcom{update/change values function}
%\alt \nont{tycon} \sym{.} \sym{\{}\nont{varid} \sym{<-} \nont{expr}\sym{\}} \gcom{change value function}
  \alt \nont{primary}\sym{.} \sym{\{}\nont{varid} \sym{?}\sym{\}} \gcom{field existence check}
  \alt \nont{primary}\sym{.} \sym{\{}\nont{varid} \sym{=}\sym{\}} \gcom{update field in value function}
  \alt \nont{primary}\sym{.} \sym{\{}\nont{varid} \sym{<-}\sym{\}} \gcom{change field in value function}
  \alt \nont{primary}\sym{.} \sym{\{}\liste{\nont{field}}{\sym{,}}\sym{\}} \gcom{value update/change}
  \alt \nont{primary}\sym{.} \bracka \nont{expr}\brackz \gcom{array element selection}
  \alt \term{\_}\sym{.} \nont{varid} \gcom{anonymous member application}
% \alt \nont{primary} \sym{.} \bracka \nont{expr} \sym{=} \nont{expr}\brackz \gcom{array update}
% \alt \nont{primary} \sym{.} \bracka \nont{expr} \sym{<-} \nont{expr}\brackz \gcom{destructive array element update}\\
  \alt \texttt{do} \bracea{} \liste{\nont{dlcqual}}{\sym{;}} \bracez{} \gcom{monadic expression}
  \alt \nont{term}\\
\rul{field} \nont{varid} \sym{=} \nont{expr} \gcom{field update}
  \alt \nont{varid} \sym{<-} \nont{expr} \gcom{field change}
  \alt \nont{varid} \gcom{field update with punning}
\end{flushleft}

The syntax reveals that the \sym{.} works like a left associative operator. This is so that primary expressions can be chained, much like in conventional programming languages. For example \ex{persons.[42].age.negate} could be the negated value associated with the \texttt{age} field of the value at index 42 of the \texttt{persons} array.

\subsection{Special interpretation of the dot}

The single symbol \sym{.} as syntactic element used to form primary expression will only be recognized if the following conditions all hold:

\begin{itemize}
\item it is not surrounded by white space on both sides (line breaks count as whitespace)
\item the previous token, if any, is not \sym{(}
\item the next token, if any, is not \sym{)}
\end{itemize}

In all other cases, a single \sym{.} will be recognized as \sym{$\bullet$}, which is the function composition operator. 

These rules do not affect recognition of operators that contain one or more dots.

\hasdiff{The single \sym{.} is an overloaded character. If it is enclosed within spaces or if it looks like a section, it will be as if the  function composition operator \sym{$\bullet$}\footnotemark{} had been typed in its place. In all other cases, it is taken as part of a primary expression or a qualified name.

This is to maximize compatibility with \haskell{}, or to make it easy at least to port \haskell{} source code.}
\footnotetext{Unicode \term{U+2022}. Can be produced in Windows with \textsc{Alt+}\texttt{0149} (type number on the numeric keypad), in Linux depending on the input method with \textsc{Compose+}\texttt{.=}}


\subsection{Member function application} \label{memfunapp}
\index{expression!primary!member function application}

This is a convenient notation to apply functions defined locally to a name-space such as a data type or type class. This syntactic form is translated like this:

\trans{\\
\begin{tabular}{lclp{0.6\textwidth}}
$e$.$m$ & $=$ & ($T$.$m$ $e$) & if the expression $e$ has type $t$ and the type constructor of $t$ is $T$ and there exists a function $T$.$m$\\
& $=$ & ($C$.$m$ $e$) & if $m$ is an overloaded function belonging to type class $C$\\
\end{tabular}\\
The conditions will be checked in the order listed here and the first possible translation will be selected. If none of the conditions hold, the compiler flags a type error.
}

Because the compiler creates functions for access to fields in \hyperref[fieldconstructor]{algebraic data types with field labels} that happen to have the same name as the field label, this syntax is most prominent for extraction of field values.

\label{confusedots}For \hyperref[qualified names]{lexical reasons}, when $e$ is a nullary value constructor such as \ex{Nothing} one cannot write for instance \ex{Nothing.show} as a shorthand for \ex{Show.show Nothing}
This is because the lexical analyzer will tokenize 
\ex{Nothing.show} as qualified variable (\nont{qvarid})
and then during name resolution \texttt{Nothing.} would be interpreted as name of a type or name space (which would probably fail).
One can avoid this by writing one of \ex{Nothing .show} (with space before the dot so as to make interpretation as qualified variable impossible) or \ex{(Nothing).show}

\subsection{Field Existence Test} \label{field existence}
\index{expression!primary!field existence}

The expression $T$.\{$field$\sym{?}\} denotes the function that checks, whether a value $v$ with a type $T u_1 \cdots u_k$  where $k>=0$ was constructed with a \hyperref[fieldconstructor]{data constructor} in whose field list the label $field$ appears.

The expression $v$.\{$field$\sym{?}\} can be used in place of  ($T$.\{$field$\sym{?}\} $v$) if the type of $v$ is already known. The type of $v$ can not be inferred from the former expression, only from the latter one.

\trans{
%\begin{flushleft}
Let it be known that $v$ is of type $t$, and let $t$ be an algebraic data type with constructors $C1$, $C2$ and $C3$. Let label $field$ appear in $C1$ and $C2$. Then the following transformation can be applied:\\
%\end{flushleft}
\begin{tabular}{lclp{0.6\textwidth}}
$T$.\{$field$?\} & $=$ & \sym{$\backslash$}$v$ $\rightarrow$ case $v$ of \{ &\\
& & $C1 \cdots  \rightarrow$ \textbf{true};  & \\
& & $C2 \cdots  \rightarrow$ \textbf{true}; &  \\
& & $C3 \cdots  \rightarrow$ \textbf{false}  \} & \\
$v$.\{$field$?\} & $=$ & ($T$.\{$field$?\} $v$) & -- if $v$ has type $T u_1 \cdots u_k$ \\
\end{tabular}
~\\
The $\cdots$ following the constructors represent the correct number of \_-patterns for the respective constructor.
}

If ($T$.\{$field$\sym{?}\} $v$) returns \term{true}, all field update and access functions for $field$ can be applied to $v$. If it is \term{false}, however, application of any of those functions results in a pattern match failure.

\begin{figure}[hbt]
\begin{code}
data T = C1 {name::String, age::Int}
chgName :: T -> String -> T
chgName = T.{name=}
nullifyName :: T -> T
nullifyName = T.{name=""}
age10Factory :: String -> T  -- with age = 10
age10Factory = C1 {name="", age=10}.{name=}
incrAge :: Int -> T -> T
incrAge n = T.{age <- (n+)}
\end{code}
\caption{Some primary expressions and their types}
\label{primexprexample}
\end{figure}


\subsection{Value Update and Change by Field Label} \label{fiieldupd}
\index{expression!primary!update by field}

The expression $T$.\{$field$=\} denotes a function that, when applied to two values $v$ and $u$, creates a new value of type $T u_1 \cdots u_k$  (where $k>=0$) that differs from $v$ only in the value for field $field$, which is set to $u$.
This implies that $v$ is also of type $T u_1 \cdots u_k$  (where $k>=0$) and $u$ of the type that was given for label $field$ in the declaration of $T$.

The expression $T$.\{$field$$\leftarrow$\} denotes a function that, when applied to two values $v$ and $g$, creates a new value of type $T u_1 \cdots u_k$  (where $k>=0$) that differs from $v$ only in the value for field $field$, which is set to the result of $g$ applied to the value of $field$ in $v$.
This implies that $v$ is also of type $T u_1 \cdots u_k$  (where $k>=0$) and $g$ of the type ($t \rightarrow t$), where $t$  was the type given for label $field$ in the declaration of $T$.

In both cases, $v$ must have been constructed with a \hyperref[fieldconstructor]{data constructor} in whose field list  the label $field$ appears. Otherwise, the result is undefined, and an attempt to evaluate it will cause a pattern match failure.

\begin{figure}[hbt]
\trans{
Let it be known that $v$ is of type $T$, and let $T$ be an algebraic data type with data constructors $C_1$, $C_2$ and $C_3$. Let label $f$ appear as the first of two fields in $C_1$ and as the second of three fields in $C_2$\footnotemark{}. Then the following transformation is applied:\\
\begin{tabular}{lcp{0.6\textwidth}}
$T$.\{$f$=\} & $=$ & $\backslash v\backslash u \rightarrow$ \textbf{case} $v$ \textbf{of \{} \\
& & \hspace{0.25cm} $C_1$ $a_1$ $a_2 \rightarrow C_1$ $u$ $a_2$;\\
& & \hspace{0.25cm} $C_2$ $a_1$ $a_2$ $a_3 \rightarrow C_2$ $a_1$ $u$ $a_3$ \textbf{\}}\\
$T$.\{$f$$\leftarrow$\} & $=$ & $\backslash v\backslash g \rightarrow$ \textbf{case} $v$ \textbf{of \{} \\
& & \hspace{0.25cm} $C_1$ $a_1$ $a_2 \rightarrow C_1$ ($g$ $a_1$) $a_2$;\\
& & \hspace{0.25cm} $C_2$ $a_1$ $a_2$ $a_3 \rightarrow C_2$ $a_1$ ($g$ $a_2$) $a_3$ \textbf{\}}\\
$v$.\{$f$=\} & $=$ & ($T$.\{$f$=\} $v$)\\
$v$.\{$f$$\leftarrow$\} & $=$ & ($T$.\{$f$$\leftarrow$\} $v$)\\
$T$.\{$f=u$\} & $=$ & (flip $T$.\{$f$=\} $u$) \\
$T$.\{$f\leftarrow g$\} & $=$ & (flip $T$.\{$f\leftarrow$\} $g$) \\
flip $f$ $a$ $b$ & $=$ & $f$ $b$ $a$  -- standard function\\
$v$.\{$f=u$\} & $=$ & ($T$.\{$f$=\} $v$ $u$)\\
$v$.\{$f\leftarrow g$\} & $=$ & ($T$.\{$f\leftarrow$\} $v$ $g$)\\
$v$.\{$f_1=u_1$, & $=$ & $v$.\{$f_1=u_1$\} -- general rules for chained changes/updates\\
\hspace{0.5cm}$f_2\leftarrow u_2$,  &  & \hspace{0.5cm}.\{$f_2\leftarrow u_2$\}\\
\hspace{0.5cm}$f_3=u_3$, $\cdots$\} & & \hspace{0.5cm}.\{$f_3=u_3$\}. $\cdots$\\
$T$.\{$f_1=u_1$, & $=$ & $T$.\{$f_1=u_1$\}\\
\hspace{0.5cm}$f_2\leftarrow u_2$,  &  & \hspace{0.5cm}$\bullet$ $T$.\{$f_2\leftarrow u_2$\}\\
\hspace{0.5cm}$f_3=u_3$, $\cdots$\} & & \hspace{0.5cm}$\bullet$ $T$.\{$f_3=u_3$\} $\bullet$ $\cdots$\\
\end{tabular}    
\par The $a_i$ are auxiliary variables appearing nowhere else in the program. 
\par The identities make it clear that values constructed with $C_3$ cannot be changed or updated, as this constructor has no field $f$.
}
\caption{Translation of change/update primary expressions}
\label{transupdate}
\end{figure}
\footnotetext{
We pick here an arbitrary case for demonstrating purposes. The translation works no matter how many constructors exists, how many of them have a certain field and how many other fields exist. It is precisely the independence of the actual  representation of the values (viz. the type signatures of the constructors) that make the label notation a valuable feature.
}

The update and change functions are created by the compiler whenever an \hyperref[algdcl]{algebraic data type} has a constructor with field labels. They are employed by several forms of the primary expression, whose translation is given in \autoref{transupdate}.

The last 2 rules of  \autoref{transupdate} show that many changes and updates can be mixed in one pair of braces. 

As before, in constructs like $v$.\{$field \cdots$\} where $v$ is an expression, the type of $v$ can not be determined from that construct alone by the type checker. The type of $v$ must be known, either trough a \hyperref[annotation]{type annotation} or the type of $v$ must be unambiguously clear for other reasons.  


\subsection{Array Element Selection} \label{arrayop}
\index{expression!primary!indexed element access}

If $v$ denotes a native array (see ....) and $i$ an integer value, then $v.[i]$ is the value at the index given by $i$. This is safe only for arrays of primitive types, as arrays of reference types can contain \ex$null$. Note that the JVM performs index checking and will throw a runtime exception if $i$ is smaller than 0 or greater or equal to the length of the array.

\subsection{Monadic Expression} \index{expression!do}

A \emph{monadic expression} provides syntactic sugar for application of the monadic operators \sym{>>} and \sym{>>=}. Note that the qualifiers share the same syntax with list comprehensions qualifiers but that the translation is quite different.

It is transformed  according to the following rules:

\trans{\\
\begin{tabular}{lcl}
\texttt{do \{} $e$ \texttt{\}} & $=$ & $e$\\
\texttt{do \{} $e$; $q_2$; $\cdots$; $q_i$ \texttt{\}} & $=$ &
$e$ \sym{>>}  \texttt{do \{} $q_2$; $\cdots$; $q_i$ \texttt{\}}\\
\texttt{do \{} $p$ $\leftarrow$ $e$ ; $q_2$; $\cdots$; $q_i$ \texttt{\}} & $=$ &
$e$ \sym{>>=}  ($\backslash p$ \arrow{} \texttt{do \{}  $q_2$; $\cdots$; $q_i$ \texttt{\}}) \\
\texttt{do \{ let \{} $d_1$; $\cdots$; $d_i$ \texttt{\}}; & & \\
\hspace{1.5cm} $q_2$; $\cdots$; $q_i$ \} & $=$ & \texttt{let \{} $d_1$; $\cdots$; $d_i$ \texttt{\}}\\
& & \texttt{in do} \{ $q_2$; $\cdots$; $q_i$ \}\\
\end{tabular}
\par where the $d_i$ range over local declarations, $q_2$; $\cdots$; $q_i$ is a non empty list of arbitrary qualifiers, $e$ stands for an expressions and $p$ for a pattern.
}

The first rule states that the last qualifier in a monadic expression must be an expression.
The remaining rules give the translation for each possible form of the first qualifier.

The type and meaning of the monadic operations are defined in the type class Monad and in the instances for Monad.

\section{Unary operator application} 
\index{expression!unary} \label{unaryexp}

\begin{flushleft}
\rul{unary} \nont{qunop} \nont{unary}
   \alt \nont{primary} 
\end{flushleft}

The unary operators are just functions with a funny name, however, the precedence of unary operator application is even higher than that of normal function application (see next section). This is so that one can write \ex{foo !a} and this will be parsed like \ex{foo (!a)}.


\section{Function application}  \label{funapp} \index{expression!function application}

\begin{flushleft}
\rul{appex} \nont{unary} \alt \nont{appex} \nont{unary}
\end{flushleft}

Function application is the most basic notion in a functional programming language and is written $e_1$ $e_2$.
Application associates to the left, so the parentheses may be omitted in \ex{(f x) y}.
Because $e_1$ could be a data constructor, partial applications of data constructors are possible.

\paragraph{Example}
The expression \ex{(,) 1}
denotes a function that, when applied to another expression \ex{v}, constructs the tuple \ex{(1,v)}.


\paragraph*{Functions are curried}

In \frege{}, all functions are considered \emph{curried}; that is, every function $f$ has type $t_1 \rightarrow{} t_2$ for certain types $t_1$ and $t_2$ and thus takes exactly one argument $a$ of type $t_1$ and returns a value of type $t_2$.
Data constructors are just functions, as far as expressions are concerned.
Of course, $t_2$ can itself be a function type, say $t_3 \rightarrow{} t_4$.
In that case the expression $f$ $a$ denotes a value that \emph{is} a function and can be applied to another value $b$ of type $t_3$ immediately, yielding a value of $t_4$. And so forth, ad infinitum.

To be sure, for convenience, the language supports constructs that make it look like there were functions with more than one argument.
\begin{enumerate}
\item Function types can be written $t_1 \rightarrow{} t_2 \rightarrow{} t_3 \rightarrow{} t_4$ since the function type constructor $(\rightarrow)$ is right associative. One may view this as the type of a function that takes 3 arguments.
\item Function definitions can specify more than one argument.
\item Support on the lexical and syntactic level for "binary" operators provide special support for functions that conceptually have 2 arguments.
\item The left associativity of function application itself allows us to write \texttt{f a b c d} and nothing prevents us to think of this as "passing 4 arguments to the function $f$".
\item One can always write its own functions so that they take a tuple of values, which makes function application look very much like in conventional languages, e.g. \texttt{add(1,3)}\footnote{However, this will actually create a tuple on each function call.}
\end{enumerate}

To sum it up, nothing forces a \frege{} programmer to think in terms of single argument functions only.
Yet, it is important to keep in mind that behind the scenes this is all done with single argument functions.

\subsection{Applications of Anonymous Values} \label{fieldlambda}

When the expression that denotes the function to apply is a member application, member update or member change on the anonymous variable \term{\_}, this is ranslated like this:

\trans{\\
\begin{tabular}{lcl}
\texttt{\_.}$varid $a_1$ \cdots $a_n$ & $=$ &  
\texttt{\$\backslashit -> it.$varid$ $a_1$ \cdots $a_n$ \\
\end{tabular}
}


As convenient as the primary expressions described in the previous sections are,
there are cases where even more flexibilty is required.
The following expression tries to filter the strings that start with \ex{"foo"} from a list. For this purpose, it uses the \ex{startsWith} function that is defined in type \ex{String} and has the following type:

\exq{/startsWith :: String -> String -> Bool/}

where the first argument is the string to be checked and the second one gives the prefix to look at.

\begin{code}
xs = ["foo1", "bar2", ....]
filter (flip String.startsWith "foo") xs
\end{code}

Because of the given argument order, we must use \ex{flip} to get the string argument passed by \ex{filter} to the left. And since we have no named value to form a primary expression like \ex{v.startsWith} we need to spell the type name explicitly.


\section{Operand Expressions} \label{topex}

The expressions described in this section are called \emph{operand expressions} because they appear as operands of \hyperref[binex]{infix expressions}.

\subsection{Lambda Expression} \label{lambda}
    \index{expression!lambda}

A lambda expression defines an anonymous function.

\begin{flushleft}
\rul{lambda} \sym{$\backslash$} \nont{lpats} \nont{lambda}
  \alt \sym{$\backslash$} \nont{lpats} \sym{->} \nont{expr}
\end{flushleft}

The syntax of patterns (\nont{lpats})and semantics of pattern matching are explained below, see \autoref{patternmatch}.

A lambda expression $\backslash{}p_1\rightarrow{}\backslash{}p_2 \rightarrow{}\cdots{}\backslash{}p_k \rightarrow{} e$ can be abbreviated\\ $\backslash{}p_1 \backslash{}p_2 \cdots{} \backslash{}p_k \rightarrow{} e$ or $\backslash{}p_1 p_2 \cdots{} p_k \rightarrow{} e$ 

A lambda expression $\backslash{}p \rightarrow{} e$ has type $a \rightarrow{} b$ where $a$ is the type of the pattern $p$ and $b$ the type of the expression $e$.


\trans{
Application of a lambda expression is equivalent to a case expression (see \autoref{caseex})\\
\begin{tabular}{lcl}
($\backslash{}p$ \arrow{} $b$) $e$ & = & \texttt{case} $e$ \texttt{of} $p$ \arrow{} $b$\\
\end{tabular}
\par where $b$ and $e$ are expressions and $p$ is a pattern.
}

\subsection{Conditional} \label{conditional} \index{expression!conditional}

\begin{flushleft}
\rul{cond} \term{if} \nont{expr} \term{then} \nont{expr} \term{else} \nont{expr}\\
\end{flushleft}

A conditional expression \texttt{if} $e_1$ \texttt{then} $e_2$ \texttt{else} $e_3$ returns $e_2$ if $e_1$ evaluates to \texttt{true}, $e_3$ if $e_1$ is false and is undefined in all other cases.

The condition $e_1$ has type \texttt{Bool} and the possible results have the same type which is also the type of the whole expression.

\subsection{Let Expressions} \index{expression!let} \label{letexpr}

\begin{flushleft}
\rul{letex} \term{let} \bracea{} \liste{\nont{decl}}{\sym{;}} \bracez{} \term{in} \nont{expr}
\end{flushleft}

Let expressions have the general form
\texttt{let \{} $d_1 ; \cdots{} ; d_n$  \texttt{\} in} $e$,
and introduce a nested,
lexically-scoped, mutually-recursive list of declarations
(let is often called letrec in other languages).
The scope of the declarations is the expression $e$ and the right hand side of the declarations.

Declarations appropriate for use in \texttt{let} expressions are described in \autoref{decl}. The semantics of the nested declarations are described in \autoref{letsemantics}.

Pattern bindings are matched lazily, for example \mint{fr}{let (a,b) = (3 `div` 0, 42) in b+1} will not cause an execution time error until \texttt{a} is evaluated.

The value computed by $expr$ is also the value of the whole let expression. It follows, that the type of the let expression is the type of $expr$.

\subsection{Case Expressions} \label{caseex} \index{expression!case}

\begin{flushleft}
\rul{casex} \term{case}  \nont{expr} \term{of} \bracea{} \liste{\nont{alt}}{\sym{;}} \bracez{}\\
\rul{alt} \nont{pattern} \sym{->} \nont{expr}
  \alt \nont{pattern} \nont{guarded-exs}
  \alt \nont{alt} \term{where} \bracea{} \liste{\nont{decl}}{\sym{;}} \bracez{}\\
\rul{guarded-exs} \more{\nont{guarded-ex}}\\
\rul{guarded-ex} \sym{$|$} \liste{\nont{lc-qual}}{\sym{,}} \sym{=} \nont{expr}
\end{flushleft}

A case expression has the general form
\begin{center}
\texttt{case} $e$ \texttt{of \{} $p_1$ $match_1$; $\cdots$; $p_n$ $match_n$ \texttt{\}}
\end{center}
where each $match_i$ is of the general form
\begin{center}
\texttt{$|$} $gd_{i_1}$ \texttt{=} $e_{i_1}$
\texttt{$|$} $\cdots$
\texttt{$|$} $gd_{i_m}$ \texttt{=} $e_{i_m}$
\texttt{where \{} $decls_i$ \texttt{\}}
\end{center}
Each alternative $p_i$ $match_i$ consists of a pattern $p_i$ and its matches, $match_i$, which consists of pairs of guards $gd_{i_j}$ and bodies $e_{i_j}$, as well as optional bindings ($decls_i$) that scope over all of the guards and expressions of the alternative.
An alternative of the form
\begin{center}
\nont{pat} \texttt{->} \nont{expr} \texttt{where \{} \nont{decls} \texttt{\}}
\end{center}
is treated as shorthand for:
\begin{center}
\nont{pat} \texttt{$|$ true =} \nont{expr} \texttt{where \{} \nont{decls} \texttt{\}}
\end{center}


A case expression must have at least one alternative and each alternative must have at least one body.
Each body must have the same type, and the type of the whole expression is that type.

A guard is a list of expressions of type \texttt{Bool} or submatches of the form
\begin{center}
\nont{pat} \texttt{$\leftarrow$} \nont{expr}
\end{center}
The expressions will be evaluated in the environment of the case expression extended by the bindings created during the matching of the alternative.
The submatches may themselves create new bindings, these will be in scope for subsequent submatches of the same guard and for the expression associated with that guard.

A guard is matched successful if all expressions yield the result \texttt{true} and all submatches succeed.
A failed match or an expression that evaluates to \texttt{false} causes the next guard to be tried if there is one, otherwise the alternative is not taken.

A case expression is evaluated by pattern matching the expression $e$ against the individual alternatives.
The matches are tried sequentially, from top to bottom.
The first successful match causes evaluation of the expression that is associated with the guard that matched.
If no match succeeds, the result is undefined and the program terminates.
Pattern matching is described in \autoref{patternmatch}, with the formal semantics of case expressions
in \autoref{formalcase}.

\section{Infix Expressions} \label{binex}
\index{expression!infix or binary}

Infix expressions are applications of infix operators (see \autoref{operator}) written in natural notation. We also speak of  \emph{binary} expressions or operators.

\begin{flushleft}
\rul{binex} \nont{binex$_{1}$}\\
\rul{binex$_{17}$} \nont{operand}\\
\rul{binex$_i$}
        \nont{binex$_i$}     \nont{opleft$_i$}  \nont{binex$_{i+1}$}
   \alt \nont{binex$_{i+1}$} \nont{opright$_i$} \nont{binex$_i$}
   \alt \nont{binex$_{i+1}$} \nont{opnone$_i$}  \nont{binex$_{i+1}$}
   \alt \nont{binex$_{i+1}$}\\
\rul{opleft$_i$}   \nont{lexop$_i$} \gcom{left associative with precedence $i$}\\
\rul{opright$_i$}  \nont{lexop$_i$} \gcom{right associative with precedence $i$}\\
\rul{opnone$_i$} \nont{lexop$_i$} \gcom{non-associative with precedence $i$}\\
\end{flushleft}

The syntax shows that operand expressions have higher precedence than any binary expression, followed by binary expressions of precedence 16 down to 1.

\trans{\\
\begin{tabular}{lcl}
$e_1$ `op` $e_2$ & $=$ & (`op`) ($e_1$) ($e_2$)
\end{tabular}
}

\begin{figure}[hbt]
\begin{code}
infixr 16  • 
infixr 15  ^ 
infix  15  ~~* ~~~ ~ ~~ =~~ =~ !~ 
infixl 14  rem quot mod div / * 
infixr 13  mplus <+> ++ 
infixl 13  - + 
infix   9  notElem elem >= > <= < 
infix   8  compare <=> 
infix   7  === == /= != !== 
infixr  6  und && 
infixr  5  || oder ^^ 
infixr  4  : !: 
infixl  4  fmap <* <$> <*> *> 
infixr  3  >=> <=< 
infixl  3  >>= >> <|> 
infixr  2  seq @ =<< 
infixl  2  finally either catch 
infixr  1  $! $ 
infixl  1  on
\end{code}
\caption{Prelude Standard Operators} \label{predefops}
\end{figure}

However, care must be taken with certain \emph{left} operands, like:

\exq/if a then b else c   + 1/

Because the \hyperref[annex]{expression} after the \term{else} extends as far as syntactically possible, this is equivalent to

\exq/if a then b else (c + 1)/

On the other hand, a \emph{right} operand often works like expected:

\exq/1 + if a then b else c/

In any case, it is certainly a good idea to write explicit parentheses whenever there is the slightest doubt about the possible parsing of an infix expression. 

\section{Annotated Expression} \label{annex}

\begin{flushleft}
\rul{expr} \nont{topex} \sym{::} \nont{sigma} \alt{} \nont{topex}\\
\rul{topex} \nont{casex} \alt{} \nont{letex} \alt{} \nont{cond} \alt{} \nont{lambda} \alt{} \nont{binex} \\
\end{flushleft}

An expression may be annotated with a type, the notation $e$ :: $t$ means literally \emph{expression} $e$ \emph{has type} $t$. If $e$ has indeed this type, or a more general one, the value $e$ will be computed at the given type, otherwise the compiler will flag an error.

\paragraph{Example}
The expression on the right hand side of the function definition

\exq/foo a b c = a+b-c/

has type 
\ex/Num a => a/, that is, it can have any type that is an instance of type class Num. However, if one writes

\exq/foo a b c = a+b-c :: Int/

this restricts the type to Int.



\section{Pattern Matching} \label{patternmatch} \index{pattern} 

Patterns appear in lambda abstractions, function definitions, pattern bindings, list comprehensions, do expressions, and case expressions. However, the first five of these ultimately translate into case expressions, so defining the semantics of pattern matching for case expressions is sufficient.

\subsection{Patterns} \label{patterns} \index{pattern!syntax}

Patterns have this syntax:

\begin{flushleft}
\rul{pattern} \nont{pattern} \sym{::} \nont{sigma} \alt{} \nont{atpattern}\\
\rul{atpattern} \nont{pvar} \sym{@} \nont{atpattern}
  \alt \nont{listpattern}\\
\rul{listpattern} \nont{matcherpattern} \sym{:} \nont{listpattern}
  \alt \nont{matcherpattern}\\
\rul{matcherpattern} \nont{pvar} \sym{\symbol{126}} \nont{regexliteral}
  \alt \nont{pconapp} \\
\rul{pconapp} \nont{pconapp} \nont{strictpattern}
  \alt \nont{strictpattern}\\
\rul{strictpattern} \sym{!} \nont{pterm} \alt{} \nont{pterm} \\
\rul{pterm} \nont{conid}    \gcom{constructor}
    \alt \nont{conid} \sym{\{} \opt{\nont{patternfields}} \sym{\}}
    \alt \nont{pvar}        \gcom{variable, possibly strict}
    \alt \nont{literal}
    \alt \sym{(} \sym{)}    \gcom{unit constructor}
    \alt \sym{[} \sym{]}           \gcom{empty list}
    \alt \sym{[} \liste{\nont{pattern}}{\sym{,}} \sym{]} \gcom{literal lists}
    \alt  \sym{(} \nont{pattern}\sym{,} \liste{\nont{pattern}}{\sym{,}}\sym{)}       \gcom{tuples}
    \alt \sym{(} \nont{pattern} \sym{)}\\    

 \rul{pvar} \nont{varid}   \gcom{variable}
    \alt \regex{\_}           \gcom{anonymous variable}\\

\rul{lpats} \more{\nont{strictpattern}}

\rul{patternfields} \liste{\nont{varid}\sym{=}\nont{pattern}}{\sym{,}}\\
\end{flushleft}

The pattern syntax is complicated at first sight only. A pattern is, syntactically, just a binary expression (see \autoref{binex}) with the following restrictions:
\begin{itemize}
\item the only infix operators allowed are \sym{@}, \sym{\symbol{126}}, \sym{:} and constructors written in infix notation.
\item only constructor applications are allowed
\item no partial applications are allowed
\item the only unary operator is \sym{!}
%\item the only primary pattern is the record update/record member pattern.
\item pattern tuples and lists are similar in appearance to their expression counterparts, except that they are made up of subpatterns instead of subexpressions. They are just syntactic convenient ways to write constructor applications.
\end{itemize}

In a constructor application pattern, the arity of the constructor must match the number of sub-patterns associated with it; one cannot match against a partially-applied constructor.

In contrast to expressions, constructors with field lists do not have to list all fields. It is even possible to have an empty pattern field list. A constructor with field list is transformed to an ordinary constructor application. The translation inserts anonymous variables for all missing fields.

All patterns must be linear - no variable may appear more than once. For example, this definition is illegal:
\mint{hs}{f (x,x) = x -- ILLEGAL; x used twice in pattern}

Patterns of the form $pat$::$type$ assert that the value matched with $pat$ must have type $type$.
Patterns of the form
$var$@$pat$
are called as-patterns, and allow one to use
$var$
as a name for the
value being matched by $pat$. For example, the following function to "sort" a tuple
\mint{hs}{\(a,b) -> if b<a then (b,a) else (a,b)}
constructs a new value that is equal to the original one in the else clause. To reuse the original value, one could write
\mint{hs}{\(orig@(a,b)) -> if b<a then (b,a) else orig}
which is equivalent to
\mint{hs}{\orig -> case orig of (a,b) -> if b<a then (b,a) else orig}

Patterns of the form \_ are wildcards and are useful when some part of a pattern is not referenced on
the right-hand-side. It is as if an identifier not used elsewhere were put in its place.

\subsection{Informal Semantics of Pattern Matching} \index{pattern!matching}

Patterns are matched against values. Attempting to match a pattern can have one of three results: it may \emph{fail}, it may \emph{succeed}, or it may \emph{diverge}
\footnote{A match \emph{diverges} if, according to the described rules, the pattern requires evaluation of the matched value and the result of that evaluation turns out to be undefined.}.
When the match succeeds, each variable in the pattern will be bound to a value.

Pattern matching proceeds from left to right, and outside to inside, according to the following rules:

\begin{enumerate}
\item Matching a variable $p$ against a value $v$ always succeeds and binds $p$ to $v$.
\item Matching the wildcard pattern \_ against any value succeeds and no binding is done.
\item Matching a pattern of the form $pat$::$t$ against a value $v$ matches $pat$ against $v$.
\item Matching a pattern of the form $pvar$@$pat$ against a value $v$ matches $pat$ against $v$, and if this succeeds, binds $pvar$ to $v$.
\item Matching a pattern $C$ $p_1$ $\cdots$ $p_k$ against a value $v$, where $C$ is a constructor depends on the value:
\begin{itemize}
\item If $v$ is of the form $C$ $v_1$ $\cdots$ $v_k$ ($0\le k\le 26$), the sub-patterns $p_i$ are matched left to right against the components $v_i$; if all matches succeed, the overall match succeeds; the first to fail or diverge causes the overall match to fail or diverge, respectively.
\item If $v$ is of the form $C'$ $v_1$ $\cdots$ $v_n$, where $C'$ is a different constructor to $C$, the match fails.
\item If the value is undefined, the match diverges.
\end{itemize}
Constructors with arity 0 are just a special case without sub-matches.

Constructor application patterns with field lists will have been transformed to ordinary constructor application patterns. Only the named field's subpattern will be matched against the corresponding subvalues. If the pattern field list is empty, just the constructor is checked.
\item Matching a boolean, numeric, string or character literal against a value succeeds if the value equals the value represented by the literal. It diverges if the value is undefined. Otherwise, the match fails.
\item Matching a regular expression literal (see \autoref{regexliteral}) against a value of type \texttt{String} diverges if the value is undefined. It succeeds, if the regular expression matches the string and fails otherwise.
\item If the pattern is of the form $m$\symbol{127}\#$re$\# it will be checked whether the regular expression matches the string as before and when this is the case, the variable $m$ is bound to the matcher employed in the regular expression match. This, in turn, makes it possible to access the matched substring as well as the matched substrings corresponding to any parenthesized groups in the regular expression:
\begin{code}
case "John Smith" of
    m~#(\w+)\s+(\w+)# -> case (m.group 1, m.group 2) of
             (Just a, Just b) -> b ++ ", " ++ a  -- "Smith, John"
\end{code}
\item \label{strictpats} A strict pattern \sym{!}$p$ is matched against a value $v$ by first evaluating $v$ and then matching $p$ against the result. Because evaluation of a value can diverge, matching a strict pattern can diverge in cases  when matching a normal pattern would not. This can change the semantics of a program as the following example shows:
\begin{code}
swap1 (a,b)   = (b,a)
swap2 (!a, b) = (b,a)
ex1 = swap1 (7 `div` 0, 42)   -- yields (42, 7 `div` 0)
ex2 = swap2 (7 `div` 0, 42)   -- diverges
\end{code}

The strict pattern is helpful when the expression can be evaluated efficiently enough to outweigh the imposed cost of laziness:

\begin{code}
-- drop the first n elements from a list
drop n xs = case xs of
    [] -> []
    _:ys -> if n > 0 then drop (n-1) ys else xs
\end{code}

Here, the value $n$ will not be evaluated if the list is empty, thus the application \texttt{drop (7 `div` 0) []} would compute the correct answer (the empty list). But for nonempty lists, $n$ will be evaluated due to the comparison with 0. By making $n$ a strict variable, the function will probably perform better in the vast majority of cases, however, the application above would then cause the program to abort.

\end{enumerate}
\trans{
Matches with regular expressions are translated like this:\\
\begin{tabular}{lcl}
\texttt{case} $v$ \texttt{of} \symbol{35}$rx$\symbol{35} \arrow{} $e$ &
$=$ &
\texttt{case} $v$ \texttt{of} $s$ $|$ $s$ \symbol{126} \#$rx$\# \arrow{}
$e$\\
\texttt{case} $v$ \texttt{of} $m$\symbol{126}\#$rx$\# \arrow{} $e$ &
$=$ &
\texttt{case} $v$ \texttt{of}\\
& &\hspace{0.25cm}$s$ $|$ Just $m$ $\leftarrow$ $s$ =\symbol{126} \#$rx$\# \arrow{} $e$\\
\end{tabular}

where $rx$ stands for the regular expression and $s$ is a fresh variable. (\symbol{126}) is a function defined in the Prelude that checks whether a string is matched by a regular expression.
(=\symbol{126}) is a function defined in the prelude that performs a regular expression match and returns a result of type \texttt{Maybe Matcher}.
}
\subsubsection{Pattern matches that force evaluation}
Some pattern matches force evaluation of the value matched:
\begin{itemize}
\item all literal patterns and $m$\symbol{126}\#$rx$\# need to fully evaluate the value.
\item constructor application patterns for non-product types force evaluation of the value so that the constructor is known.
\item strict patterns forces evaluation of the value in all cases, even if it has a product type. However, subcomponents of the value (if there are any) are not evaluated.
\end{itemize}

\paragraph{Example}
In the example of the drop function above, the constructor patterns for the list argument force the list passed as argument to be evaluated so that the pattern match can see if it is an empty list or a list with at least one element.

\subsubsection{Irrefutable patterns}

A pattern is said to be irrefutable if the match cannot possibly fail. Except for the case of patterns with constructors, the corresponding values need not be evaluated during matching.

\begin{itemize}
%\item Patterns that cause evaluation of the value matched are not irrefutable, because the match can diverge.
\item Non-strict variable and wildcard patterns are irrefutable.
\item $p$::$t$ is irrefutable, if $p$ is
\item $v$@$p$ is irrefutable if $p$ is
\item $C$ $p_0$ $\cdots$ $p_k$ is irrefutable if all sub patterns are irrefutable and if $C$ is the only constructor of the algebraic data type. Note that even if no variables bound in sub patterns  are ever used in their scope, the value will be evaluated.
\item All other patterns are refutable.
\end{itemize}

\hasdiff{There exists no syntax to force a pattern to be irrefutable.}

\subsection{Formal Semantics of Case Expressions}

The semantics of all pattern matching constructs other than \texttt{case} expression is defined by giving identities that relate those constructs to \texttt{case} expressions. The semantics of \texttt{case} expressions themselves are in turn given as a series of identities, in \autoref{formalcase}. Implementations will behave so that these identities hold; this is not to say that they must use them directly, since that would generate rather inefficient code.

In \autoref{formalcase} $e$, $e'$ and $e_i$ are expressions; $g$ and $g_i$ are guards; $q$ and $q_i$ are qualifiers; $p$ and  $p_i$ are patterns; $v$, $x$ and $x_i$ are variables; $y$ is a fresh variable with a name that differs from all other names in the program; $C$ and $C'$ are algebraic data type constructors (including tuple, list and record constructors); $r$ is a regular expression literal and $k$ is a boolean, character, string or numeric literal.

\begin{figure}[hbt]
\fbox{
\begin{tabular}{ll}
(a) & \texttt{case} $e$ \texttt{of} \{ $p_1$ $match_1$; $\cdots$; $p_n$ $match_n$ \}\\
&$=$ \texttt{case} $e$ \texttt{of} \{ $p_1$ $match_1$; \_ \arrow{} \texttt{case} $e$ \texttt{of} \{ $p_2$ $match_2$; $\cdots$; $p_n$ $match_n$ \}\}\\
& where each $match_i$ has the form\\
& $|$ $g_{i,1}$ \arrow{} $e_{i,1}$ $|$ $\cdots$ $|$ $g_{i,m}$ \arrow{} $e_{i,m}$ \texttt{where} \{ $decls_i$ \}\\
(b) & \texttt{case} $e$ \texttt{of} \{ $p_1$ $match_1$ \}\\
&$=$ \texttt{case} $e$ \texttt{of} \{ $p_1$ $match_1$; \_ \arrow{} \texttt{error "pattern match failure"} \}\\
(c) &\texttt{case} $e$ \texttt{of} \{\\
&\hspace{0.5cm}$p$ $|$ $g_1$ \arrow{} $e_1$ $|$ $\cdots$ $|$ $g_n$ \arrow{} $e_n$  \texttt{where} \{ $decls$ \};\\
&\hspace{0.5cm}\_ \arrow{} $e'$ \}\\
&$=$  \texttt{case} $e'$ \texttt{of} \{ $y$ \arrow{} \\
&\hspace{0.5cm}\texttt{case} $e$ \texttt{of} \{ $p$ \arrow{} \texttt{let} \{ $decls$ \} \texttt{in}\\
&\hspace{1.0cm}\texttt{case} () \texttt{of} \{ () $|$ $g_1$ \arrow{} $e_1$;\\
&\hspace{3.0cm}\_ \arrow{} $\cdots$ \texttt{case} () \texttt{of} \{ () $|$ $g_n$ \arrow{} $e_n$;\\
&\hspace{7.0cm}\_ \arrow{} $y$; \} $\cdots$ \} \\
&\hspace{2.0cm}\_ \arrow{} $y$; \}\}\\
(d) &\texttt{case} () \texttt{of} \{ () $|$ $q_1$, $\cdots$, $q_n$  \arrow{} $e$; \_ \arrow{} $e'$ \}\\
&$=$  \texttt{case} $e'$ \texttt{of} \{ $y$ \arrow{} \\
&\hspace{0.75cm}\texttt{case} () \texttt{of} \{ () $|$ $q_1$ \arrow{} $\cdots$ \texttt{case} () \texttt{of} \{ () $|$ $q_n$ \arrow{} $e$;\\
&\hspace{7.0cm}\_ \arrow{} $y$; \} $\cdots$ \\
&\hspace{2.0cm}\_ \arrow{} $y$; \}\}\\
(e) &\texttt{case} () \texttt{of} \{ () $|$ $e_0$ \arrow{} $e$  ; \_ \arrow{} $e'$ \}\\
&$=$\texttt{if} $e_0$ \texttt{then} $e$ \texttt{else} $e'$\\
(f) &\texttt{case} () \texttt{of} \{ () $|$ ($e_0$ $\leftarrow$ $p_0$) \arrow{} $e$  ; \_ \arrow{} $e'$ \}\\
&$=$\texttt{case} $e_0$ \texttt{of} \{ $p_0$ \arrow{} $e$; \_ \arrow{} $e'$ \}\\
\end{tabular}
}
\caption{Identities for \texttt{case} expressions}
\label{formalcase}
\end{figure}

Rule (a) matches a general source-language \texttt{case} expression, regardless of whether it actually includes guards - if no guards are written, then \texttt{$|$true} is substituted. Also, the \texttt{where} clause may be missing, this will be equivalent to a \texttt{where} clause with 0 declarations. The rule simplifies a \texttt{case} expression with more than 1 alternatives into a nested \texttt{case} expression where each has at most 2 alternatives.

Rule (b) then supplements a \texttt{case} expression that has exactly one alternative with a catch-all alternative that evaluates to the undefined value. This guarantees that the  \texttt{case} expression evaluates to the undefined value when all matches fail.

From here on, we have to deal with \texttt{case} expressions that have exactly two alternatives, where the second alternative has a simple wild card pattern without guards and no \texttt{where} clause.

Rule (c) simplifies further by reducing multiple pattern guards to nested  \texttt{case} expressions. The construction \texttt{case () of () \arrow{} $\cdots$} indicates that these  \texttt{case} expressions do no pattern matching, but are just used to look at the guards. They are the only places where guards appear after the translation.

Our  \texttt{case} expressions now have only patterns without guards or a ()-pattern with exactly one guard and no \texttt{where} clauses. A guard may be a list of qualifiers, they are further reduced to nested  \texttt{case} expressions where guards consist of exactly one qualifier in rule (d).

Finally, rules (e) and (f) resolve the single-qualifier-guards. If the guard is a boolean expression, the \texttt{case} expression is transformed into a conditional, otherwise into a \texttt{case} expression that matches the pattern from the qualifier against the expression.
